6. 命名空间与区段🔗

名字会被组织到分层的 命名空间 里，命名空间为名字的集合。在 Lean 中，命名空间是组织 API 的主要方式：它为操作提供本体论，并将相关项聚合起来。此外，虽然不是通过将名字直接放入命名空间的方式，但一些特性（比如语法扩展、实例以及属性）的效果可以被“附着”到某个命名空间。

通过将操作整理到命名空间，使得库的结构在概念上得到全局的梳理。然而，在实际的 Lean 文件中，通常并不会同等地使用所有名字。区段提供了在局部视图下组织全局名字集的方法，也能精准控制编译器选项、语言扩展、实例和属性等的作用域。区段也允许将多个声明共享的参数集中声明，并可借助 Lean.Parser.Command.variable : commandDeclares one or more typed variables, or modifies whether already-declared variables are implicit. Introduces variables that can be used in definitions within the same `namespace` or `section` block. When a definition mentions a variable, Lean will add it as an argument of the definition. This is useful in particular when writing many definitions that have parameters in common (see below for an example). Variable declarations have the same flexibility as regular function parameters. In particular they can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are bound and declare new variables at the same time; see [issue 2789] for more on this topic. In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an `include` command or are instance implicit and depend only on such variables. See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed discussion. [tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections (Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github) ## Examples ```lean section variable {α : Type u} -- implicit (a : α) -- explicit [instBEq : BEq α] -- instance implicit, named [Hashable α] -- instance implicit, anonymous def isEqual (b : α) : Bool := a == b #check isEqual -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool variable {a} -- `a` is implicit now def eqComm {b : α} := a == b ↔ b == a #check eqComm -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop end ``` The following shows a typical use of `variable` to factor out definition arguments: ```lean variable (Src : Type) structure Logger where trace : List (Src × String) #check Logger -- Logger (Src : Type) : Type namespace Logger -- switch `Src : Type` to be implicit until the `end Logger` variable {Src} def empty : Logger Src where trace := [] #check empty -- Logger.empty {Src : Type} : Logger Src variable (log : Logger Src) def len := log.trace.length #check len -- Logger.len {Src : Type} (log : Logger Src) : Nat variable (src : Src) [BEq Src] -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments def filterSrc := log.trace.filterMap fun (src', str') => if src' == src then some str' else none #check filterSrc -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String def lenSrc := log.filterSrc src |>.length #check lenSrc -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat end Logger ``` The following example demonstrates availability of variables in proofs: ```lean variable {α : Type} -- available in the proof as indirectly mentioned through `a` [ToString α] -- available in the proof as `α` is included (a : α) -- available in the proof as mentioned in the header {β : Type} -- not available in the proof [ToString β] -- not available in the proof theorem ex : a = a := rfl ``` After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis: ``` included section variable '[ToString α]' is not used in 'ex', consider excluding it ``` In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.variable 命令按需传播。

6.1. 命名空间🔗

名称中如果包含句点（不在书名号之内），则代表这是一个分层名称；句点将名称分成若干组成部分。除了最后一个组成部分外，其他所有部分都构成了命名空间，而最后一个部分才是名称本身。

命名空间用于对相关的定义、定理、类型以及其他声明进行分组。当命名空间与某个类型名称对应时，可以使用广义域标记法来访问其内容。除了整理命名，命名空间还对语法扩展、属性以及类型类实例进行分组。

命名空间与模块是正交的：模块是一起进行繁释、编译和加载的代码单元，但模块名和它所提供的名称之间并无必要的关联。模块可以包含任意命名空间下的名字，并且分层模块的嵌套结构与分层命名空间之间没有联系。

Lean 中存在一个根命名空间，一般情况下就是省略命名空间时使用的空间。可以通过以 _root_ 开头的名称显式指明根命名空间。在某些情况下（如在某个作用域或局部作用域中），否则名字会被当作相对当前环境来解释，这时就可能需要显式指定 _root_。

显式根命名空间

当前命名空间中的名字优先于根命名空间中的名字。下面这个例子中，color 在 Forest.statement 的定义中指的是

def color := "yellow"
namespace Forest
def color := "green"
def statement := s!"Lemons are {color}"
end Forest

"Lemons are green"#eval Forest.statement

"Lemons are green"

在 Forest 命名空间内，如果要引用根命名空间下的 color，则需要加上 _root_ 前缀进行限定：

namespace Forest
def nextStatement :=
  s!"Ripe lemons are {_root_.color}, not {color}"
end Forest

"Ripe lemons are yellow, not green"#eval Forest.nextStatement

"Ripe lemons are yellow, not green"

6.1.1. 命名空间与作用域

每个作用域都有一个 当前命名空间，其取值由 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令决定。关于 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令的详细介绍见作用域命令一节。在作用域中声明的名字会被加入当前命名空间。如果声明的名称由多部分组成，那么其命名空间会嵌套在当前命名空间下；声明体中的当前命名空间是该嵌套命名空间。作用域还包含一组 已打开命名空间，这些命名空间中的内容在当前作用域内无需额外限定就可直接访问。解析一个标识符时，会考虑当前命名空间和已打开命名空间。但是，被标记为受保护的声明（即带有 protected 修饰符的声明）在打开命名空间时并不会被带入作用域。关于根据当前命名空间和打开的命名空间解析标识符的规则，详见标识符作为项的一节。

当前命名空间

定义一个归纳类型，会使其构造子被置于该类型的命名空间下，例如 HotDrink.coffee、HotDrink.tea 和 HotDrink.cocoa：

inductive HotDrink where
  | coffee
  | tea
  | cocoa

在命名空间外，除非打开该命名空间，否则需要加前缀才能使用这些名字：

HotDrink.tea : HotDrink#check HotDrink.tea

HotDrink.tea : HotDrink

#check unknown identifier 'tea'tea

unknown identifier 'tea'

section
open HotDrink
HotDrink.tea : HotDrink#check tea
end

HotDrink.tea : HotDrink

如果直接在 HotDrink 命名空间中定义函数，该函数体会在当前命名空间为 HotDrink 的情况下进行繁释。这时构造子都在作用域内：

def HotDrink.ofString? : String → Option HotDrink
  | "coffee" => some coffee
  | "tea" => some tea
  | "cocoa" => some cocoa
  | _ => none

定义另一个归纳类型会新建一个命名空间：

inductive ColdDrink where
  | water
  | juice

在 HotDrink 命名空间中，可以直接定义 HotDrink.toString，无需显式前缀。而要在 ColdDrink 命名空间中定义一个函数，则需要加上 _root_ 限定，否则会变成定义 HotDrink.ColdDrink.toString：

namespace HotDrink

def toString : HotDrink → String
  | coffee => "coffee"
  | tea => "tea"
  | cocoa => "cocoa"

def _root_.ColdDrink.toString : ColdDrink → String
  | .water => "water"
  | .juice => "juice"

end HotDrink

Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令用于打开一个命名空间，使其内容可以在当前作用域内使用。打开命名空间有多种变化方式，便于灵活管理本地作用域。

syntax打开命名空间

command ::= ...
    | Makes names from other namespaces visible without writing the namespace prefix.

Names that are made available with `open` are visible within the current `section` or `namespace`
block. This makes referring to (type) definitions and theorems easier, but note that it can also
make [scoped instances], notations, and attributes from a different namespace available.

The `open` command can be used in a few different ways:

* `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in
  `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that
  `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and
  `y`.

* `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path`
  except `def1` and `def2`.

* `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and
  `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would
  be unaffected.

  This works even if `def1` and `def2` are `protected`.

* `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path
  (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`.

  This works even if `def1` and `def2` are `protected`.

* `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances],
  notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name
  available.

* `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next
  command or expression.

[scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances
(Scoped instances in Theorem Proving in Lean)


## Examples

```lean
/-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/
namespace Combinator.Calculus
  def I (a : α) : α := a
  def K (a : α) : β → α := fun _ => a
  def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z)
end Combinator.Calculus

section
  -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`,
  -- until the section ends
  open Combinator.Calculus

  theorem SKx_eq_K : S K x = I := rfl
end

-- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here)
open Combinator.Calculus in
theorem SKx_eq_K' : S K x = I := rfl

section
  -- open only `S` and `K` under `Combinator.Calculus`
  open Combinator.Calculus (S K)

  theorem SKxy_eq_y : S K x y = y := rfl

  -- `I` is not in scope, we have to use its full path
  theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl
end

section
  open Combinator.Calculus
    renaming
      I → identity,
      K → konstant

  #check identity
  #check konstant
end

section
  open Combinator.Calculus
    hiding S

  #check I
  #check K
end

section
  namespace Demo
    inductive MyType
    | val

    namespace N1
      scoped infix:68 " ≋ " => BEq.beq

      scoped instance : BEq MyType where
        beq _ _ := true

      def Alias := MyType
    end N1
  end Demo

  -- bring `≋` and the instance in scope, but not `Alias`
  open scoped Demo.N1

  #check Demo.MyType.val == Demo.MyType.val
  #check Demo.MyType.val ≋ Demo.MyType.val
  -- #check Alias -- unknown identifier 'Alias'
end
```
open openDecl

open declaration打开整个命名空间

用一个或多个标识符组成序列，会顺序将这些命名空间打开：

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident ident*

每个命名空间都相对于所有已打开的命名空间解析，得到一组命名空间。在处理下一个命名空间之前，会先顺序打开这一组命名空间的所有成员。

打开嵌套命名空间

被打开的命名空间会相对于当前已打开的命名空间进行处理。如果某个组成部分在不同的命名空间路径中同时出现，则一次 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令可以通过迭代方式将所有相关命名空间引入作用域。下面这个例子定义了多个命名空间下的名称：

namespace A -- _root_.A
def a1 := 0
namespace B -- _root_.A.B
def a2 := 0
namespace C -- _root_.A.B.C
def a3 := 0
end C
end B
end A
namespace B -- _root_.B
def a4 := 0
namespace C -- _root_.B.C
def a5 := 0
end C
end B
namespace C -- _root_.C
def a6 := 0
end C

这些名字分别是：

A.a1
A.B.a2
A.B.C.a3
B.a4
B.C.a5
C.a6

通过一次嵌套的 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令，可以将六个名字全部引入作用域：

section
open A B C
example := [a1, a2, a3, a4, a5, a6]
end

如果命令中的初始命名空间使用了 A.B，则不会打开 _root_.A、_root_.B 或 _root_.B.C：

section
open A.B C
example := [unknown identifier 'a1'a1, a2, a3, unknown identifier 'a4'a4, unknown identifier 'a5'a5, a6]
end

unknown identifier 'a1'

unknown identifier 'a4'

unknown identifier 'a5'

打开 A.B 后，A.B.C 可以作为 C 来访问，而 _root_.C 也同样如此，因此后续 open 的 C 实际会打开这两个名字。

open declaration隐藏名字

hiding 声明用来指定在打开命名空间时哪些名字不能被带入作用域。与打开整个命名空间不同的是，这时提供的标识符必须唯一地指明待打开命名空间。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident hiding ident ident*

open declaration重命名

renaming 声明允许将打开的命名空间中的部分名字重命名；在当前作用域中可用新名字访问它们。此处提供的标识符必须唯一地指定要打开的命名空间。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident renaming (ident → ident),*

ASCII 箭头（->）也可以替代 Unicode 箭头（→）。

open declaration限制引入名称

用圆括号括住一组名字表示只将括号内列出的名字带入作用域。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | ident (ident ident*)

指定的命名空间会加到当前所有已打开命名空间中，每个名字会在所有这些命名空间中查找。列出的每个名字都必须是明确且唯一的，也就是说每个名字只能在所有考虑到的命名空间中存在于唯一一处。

open declaration仅打开受限定声明

scoped 关键字用于只打开指定命名空间中的所有受限定属性、类型类实例和语法扩展，但不会将实际名字带入作用域。

`openDecl` is the body of an `open` declaration (see `open`) openDecl ::= ...
    | scoped ident ident*

打开受限定声明

下面例子中，在命名空间 NS 下定义了一个受限定的符号扩展以及一个定义：

namespace NS
scoped notation "{!{" e "}!}" => (e, e)
def three := 3
end NS

在命名空间外，这个符号扩展无法直接使用：

def x := {!{ "pear" }unexpected token '!'; expected '}'!}

<example>:1:21-1:22: unexpected token '!'; expected '}'

用 open scoped 命令后，符号扩展才能使用：

open scoped NS
def x := {!{ "pear" }!}

但是，名字 NS.three 仍然无法直接访问：

def y := unknown identifier 'three'three

unknown identifier 'three'

6.1.2. 导出名称

导出一个名字，就是将其引入到当前命名空间内。与定义不同，导出的名字是完全透明的：在使用时会直接解析到原始名字。将名字导出到根命名空间，则可以直接不加限定地访问它；Lean 标准库会这样做，例如 Option 的构造子，或像 get 这样的关键类型类方法。

syntax导出名称

export 命令可以将其他命名空间中的名字添加到当前命名空间，就好像它们原本就是在这里声明的一样。当当前命名空间被打开时，这些导出的名字也会被带入作用域。

command ::= ...
    | Adds names from other namespaces to the current namespace.

The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`:

- visible in the current namespace without prefix `Some.Namespace`, like `open`, and
- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`.

## Examples

```lean
namespace Morning.Sky
  def star := "venus"
end Morning.Sky

namespace Evening.Sky
  export Morning.Sky (star)
  -- `star` is now in scope
  #check star
end Evening.Sky

-- `star` is visible in `Evening.Sky`
#check Evening.Sky.star
```
export ident (ident*)

内部实现上，导出的名字会注册成其目标的别名。在内核看来，只有原始名字存在；繁释器在解析标识符到名字的过程中负责处理别名。

导出名称

声明归纳类型 Veg.Leafy 的同时，也声明了构造子 Veg.Leafy.spinach 和 Veg.Leafy.cabbage：

namespace Veg
inductive Leafy where
  | spinach
  | cabbage
export Leafy (spinach)
end Veg
export Veg.Leafy (cabbage)

第一次 export 命令将 Veg.Leafy.spinach 作为 Veg.spinach 引入作用域，因为此时当前命名空间是 Veg。第二次导出将 Veg.Leafy.cabbage 引入根命名空间，可以直接使用 cabbage。

6.2. 区段作用域（Section Scopes）🔗

许多命令会对当前 区段作用域产生影响（有时在明确语境下简称为“作用域”）。每个 Lean 模块都自带一个区段作用域。通过 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令、Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 命令，以及 Lean.Parser.Command.in : commandin 命令组合子，可以创建嵌套的作用域。

区段作用域中追踪如下数据：

当前命名空间（The Current Namespace）: 当前命名空间 指新声明将被定义到的命名空间。此外，名字解析包括所有当前命名空间前缀，以作为全局名字可用的作用域一部分。
已“开放”的命名空间（Opened Namespaces）: 当一个命名空间被开放时，其名字无需显式前缀即可在当前作用域可用。此外，被开放命名空间下的限定属性及作用域内语法扩展在当前区段作用域内也会生效。
选项（Options）: 编译器选项在其被更改的作用域结束时，会复原为原来的值。
区段变量（Section Variables）: 区段变量，即自动加到定义里的名字（或实例隐式参数）。当区段变量出现在定理陈述中时，也会自动加为定理的全称假设。

6.2.1. 控制区段作用域🔗

Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 命令会新建一个区段作用域，但并不会修改当前命名空间、已开放命名空间或区段变量。所有对区段作用域做出的更改，在区段结束时将被还原。区段可以选择命名；关闭区段的 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令需使用相同的名字。如果区段名含有多个部分（即有 .分隔），则会引入多层嵌套区段。区段名字不会产生其它效果，仅是为了可读性和方便重构。

syntax区段

command ::= ...
    | A `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local`
commands. Sections can be nested. `section <id>` provides a label to the section that has to appear
with the matching `end`. In either case, the `end` can be omitted, in which case the section is
closed at the end of the file.
section ident?

命名区段

名字 english 是在 Greetings 命名空间下定义的。

def Greetings.english := "Hello"

在其命名空间外无法直接访问。

#eval unknown identifier 'english'english

unknown identifier 'english'

打开一个区段可以让对全局作用域的修改被限制在其中。下例区段名为 Greetings。

section Greetings

即使区段名和定义中的命名空间一致，由于区段名字仅作为可读和重构辅助，这个名字仍未在作用域内：

#eval unknown identifier 'english'english

unknown identifier 'english'

打开 Greetings 命名空间后，Greetings.english 就能以 english 名称出现于当前作用域：

open Greetings

"Hello"#eval english

"Hello"

关闭区段时，区段的名字必须被使用：

invalid 'end', name is missing (expected Greetings)end

invalid 'end', name is missing (expected Greetings)

end Greetings

当区段被关闭时，通过 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 命令带来的影响会恢复：

#eval unknown identifier 'english'english

unknown identifier 'english'

Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令也会新建一个区段作用域。在这个区段作用域下，当前命名空间会变为所提供的名字（相对周围的当前命名空间）。如同区段一样，对区段作用域的更改会在命名空间关闭时还原。

要关闭命名空间，Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令需提供当前命名空间的某个后缀，关闭后该后缀就会被移除。所有由 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令引入、并属于该后缀的区段作用域也会一起关闭。

syntax命名空间声明

namespace 命令通过追加指定标识符来修改当前命名空间。

会创建一个区段作用域，该作用域会持续到 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令或者文件结尾为止。

command ::= ...
    | `namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
  full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
  are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
  opening the namespace.

As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.

`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
namespace ident

syntax区段与命名空间终止

不带标识符时，Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 会关闭最近打开的匿名区段。

command ::= ...
    | `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
end

W带标识符时，会关闭最近打开的区段或者命名空间。若是区段，则标识符必须是自上次 Lean.Parser.Command.namespace : command`namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside the section: * Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the full name `Nat.seventeen`. * Names introduced by `export` declarations are also prefixed by the identifier. * All names starting with `<id>.` become available in the namespace without the prefix. These names are preferred over names introduced by outer namespaces or `open`. * Within a namespace, declarations can be `protected`, which excludes them from the effects of opening the namespace. As with `section`, namespaces can be nested and the scope of a namespace is terminated by a corresponding `end <id>` or the end of the file. `namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.namespace 命令以来所打开区段名拼接的后缀。若是命名空间，则标识符必须是自上次未闭合的 Lean.Parser.Command.section : commandA `section`/`end` pair delimits the scope of `variable`, `include, `open`, `set_option`, and `local` commands. Sections can be nested. `section <id>` provides a label to the section that has to appear with the matching `end`. In either case, the `end` can be omitted, in which case the section is closed at the end of the file.section 以来当前命名空间扩展的后缀；之后当前命名空间会移除此后缀。

command ::= ...
    | `end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed
with `end <id>`. The `end` command is optional at the end of a file.
end ident

Lean.Parser.Command.mutual : commandend 用于关闭 Lean.Parser.Command.mutual : commandmutual 块，它是 Lean.Parser.Command.mutual : commandmutual 语法本身的一部分，而不是 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令。

嵌套命名空间与区段

命名空间与区段可以嵌套使用。一次 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 命令可以关闭一个或多个命名空间，或者一个或多个区段，但不能混合关闭两者。

通过两个单独命令将当前命名空间设为 A.B.C 后，可以用一次 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 指定 B.C 后缀批量关闭：

namespace A.B
namespace C
end B.C

此时，当前命名空间变为 A。

接下来，打开一个匿名区段和命名空间 D.E：

section
namespace D.E

此时，当前命名空间变为 A.D.E。此时如果试图用 Lean.Parser.Command.end : command`end` closes a `section` or `namespace` scope. If the scope is named `<id>`, it has to be closed with `end <id>`. The `end` command is optional at the end of a file.end 一次性关闭全部三者，会因为中间有区段导致失败：

invalid 'end', name mismatch (expected «».D.E)end A.D.E

invalid 'end', name mismatch (expected «».D.E)

因此需要分别终止命名空间和区段：

end D.E
end
end A

如果只需对单个命令临时开放作用域，可以使用 Lean.Parser.Command.in : commandin 命令组合子来创建单条命令的区段作用域。 Lean.Parser.Command.in : commandin 具备右结合性，可以组合多层作用域调整。

syntax局部区段作用域

in 命令组合子为单个命令引入区段作用域。

command ::= ...
    | command in
      command

利用 Lean.Parser.Command.in : commandin 创建局部作用域

可以使用 Lean.Parser.Command.in : commandin 让命名空间内容只在单个命令中可见：

def Dessert.cupcake := "delicious"

open Dessert in
"delicious"#eval cupcake

该命令之后，Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ```open 的影响即恢复：

#eval unknown identifier 'cupcake'cupcake

unknown identifier 'cupcake'

6.2.2. 区段变量（Section Variables）🔗

区段变量 指自动作为参数加到所有提及它们的声明里的参数。不论 autoImplicit 选项是否为 true，都适用。区段变量可以是隐式、严格隐式或者显式参数，实例隐式参数则有特别处理。

如果在非定理声明中遇到了区段变量，其就会被自动加为参数。其中若有 “实例隐式” 区段变量引用了该变量，它们也会被自动加上。如果新增的变量又依赖其它变量，那么那些变量也会被递归添加；这一过程会持续直到不再有新依赖为止。所有区段变量按照声明顺序，在其它参数之前加入。只有当区段变量在定理的陈述中出现时，才会被自动添加到定理。否则，如果在证明项中更改依赖区段变量，可能会导致定理陈述发生变化。

区段变量可以通过 Lean.Parser.Command.variable : commandDeclares one or more typed variables, or modifies whether already-declared variables are implicit. Introduces variables that can be used in definitions within the same `namespace` or `section` block. When a definition mentions a variable, Lean will add it as an argument of the definition. This is useful in particular when writing many definitions that have parameters in common (see below for an example). Variable declarations have the same flexibility as regular function parameters. In particular they can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are bound and declare new variables at the same time; see [issue 2789] for more on this topic. In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that changes to the proof cannot change the statement of the overall theorem. Instead, variables are only available to the proof if they have been mentioned in the theorem header or in an `include` command or are instance implicit and depend only on such variables. See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed discussion. [tpil vars]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections (Variables and Sections on Theorem Proving in Lean) [tpil classes]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in Lean) [binder docs]: https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789 on github) ## Examples ```lean section variable {α : Type u} -- implicit (a : α) -- explicit [instBEq : BEq α] -- instance implicit, named [Hashable α] -- instance implicit, anonymous def isEqual (b : α) : Bool := a == b #check isEqual -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool variable {a} -- `a` is implicit now def eqComm {b : α} := a == b ↔ b == a #check eqComm -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop end ``` The following shows a typical use of `variable` to factor out definition arguments: ```lean variable (Src : Type) structure Logger where trace : List (Src × String) #check Logger -- Logger (Src : Type) : Type namespace Logger -- switch `Src : Type` to be implicit until the `end Logger` variable {Src} def empty : Logger Src where trace := [] #check empty -- Logger.empty {Src : Type} : Logger Src variable (log : Logger Src) def len := log.trace.length #check len -- Logger.len {Src : Type} (log : Logger Src) : Nat variable (src : Src) [BEq Src] -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments def filterSrc := log.trace.filterMap fun (src', str') => if src' == src then some str' else none #check filterSrc -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String def lenSrc := log.filterSrc src |>.length #check lenSrc -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat end Logger ``` The following example demonstrates availability of variables in proofs: ```lean variable {α : Type} -- available in the proof as indirectly mentioned through `a` [ToString α] -- available in the proof as `α` is included (a : α) -- available in the proof as mentioned in the header {β : Type} -- not available in the proof [ToString β] -- not available in the proof theorem ex : a = a := rfl ``` After elaboration of the proof, the following warning will be generated to highlight the unused hypothesis: ``` included section variable '[ToString α]' is not used in 'ex', consider excluding it ``` In such cases, the offending variable declaration should be moved down or into a section so that only theorems that do depend on it follow it until the end of the section.variable 命令声明。

syntax变量声明

command ::= ...
    | Declares one or more typed variables, or modifies whether already-declared variables are
  implicit.

Introduces variables that can be used in definitions within the same `namespace` or `section` block.
When a definition mentions a variable, Lean will add it as an argument of the definition. This is
useful in particular when writing many definitions that have parameters in common (see below for an
example).

Variable declarations have the same flexibility as regular function parameters. In particular they
can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they
can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an
implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are
bound and declare new variables at the same time; see [issue 2789] for more on this topic.

In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that
changes to the proof cannot change the statement of the overall theorem. Instead, variables are only
available to the proof if they have been mentioned in the theorem header or in an `include` command
or are instance implicit and depend only on such variables.

See [*Variables and Sections* from Theorem Proving in Lean][tpil vars] for a more detailed
discussion.

[tpil vars]:
https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#variables-and-sections
(Variables and Sections on Theorem Proving in Lean) [tpil classes]:
https://lean-lang.org/theorem_proving_in_lean4/type_classes.html (Type classes on Theorem Proving in
Lean) [binder docs]:
https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.BinderInfo (Documentation
for the BinderInfo type) [issue 2789]: https://github.com/leanprover/lean4/issues/2789 (Issue 2789
on github)

## Examples

```lean
section
  variable
    {α : Type u}      -- implicit
    (a : α)           -- explicit
    [instBEq : BEq α] -- instance implicit, named
    [Hashable α]      -- instance implicit, anonymous

  def isEqual (b : α) : Bool :=
    a == b

  #check isEqual
  -- isEqual.{u} {α : Type u} (a : α) [instBEq : BEq α] (b : α) : Bool

  variable
    {a} -- `a` is implicit now

  def eqComm {b : α} := a == b ↔ b == a

  #check eqComm
  -- eqComm.{u} {α : Type u} {a : α} [instBEq : BEq α] {b : α} : Prop
end
```

The following shows a typical use of `variable` to factor out definition arguments:

```lean
variable (Src : Type)

structure Logger where
  trace : List (Src × String)
#check Logger
-- Logger (Src : Type) : Type

namespace Logger
  -- switch `Src : Type` to be implicit until the `end Logger`
  variable {Src}

  def empty : Logger Src where
    trace := []
  #check empty
  -- Logger.empty {Src : Type} : Logger Src

  variable (log : Logger Src)

  def len :=
    log.trace.length
  #check len
  -- Logger.len {Src : Type} (log : Logger Src) : Nat

  variable (src : Src) [BEq Src]

  -- at this point all of `log`, `src`, `Src` and the `BEq` instance can all become arguments

  def filterSrc :=
    log.trace.filterMap
      fun (src', str') => if src' == src then some str' else none
  #check filterSrc
  -- Logger.filterSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : List String

  def lenSrc :=
    log.filterSrc src |>.length
  #check lenSrc
  -- Logger.lenSrc {Src : Type} (log : Logger Src) (src : Src) [inst✝ : BEq Src] : Nat
end Logger
```

The following example demonstrates availability of variables in proofs:
```lean
variable
  {α : Type}    -- available in the proof as indirectly mentioned through `a`
  [ToString α]  -- available in the proof as `α` is included
  (a : α)       -- available in the proof as mentioned in the header
  {β : Type}    -- not available in the proof
  [ToString β]  -- not available in the proof

theorem ex : a = a := rfl
```
After elaboration of the proof, the following warning will be generated to highlight the unused
hypothesis:
```
included section variable '[ToString α]' is not used in 'ex', consider excluding it
```
In such cases, the offending variable declaration should be moved down or into a section so that
only theorems that do depend on it follow it until the end of the section.
variable bracketedBinder bracketedBinder*

variable 后允许的带括号参数（bracketed binders）语法与定义头的语法一致。

区段变量

在下例区段中，自动隐式参数被禁用，并定义了一组区段变量。

section
set_option autoImplicit false
universe u
variable {α : Type u} (xs : List α) [Zero α] [Add α]

由于自动隐式参数已禁用，下面这个定义会失败：

def addAll (lst : List unknown identifier 'β'β) : unknown identifier 'β'β :=
  lst.foldr (init := 0) (· + ·)

unknown identifier 'β'

另一方面，即便在定义时不写 xs，也能使用它：

def addAll :=
  xs.foldr (init := 0) (· + ·)

如果希望即使区段变量没有在定理声明里显式提及时也自动加到定理上，可以用 Lean.Parser.Command.include : command`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the theorem header. Other commands are not affected. `include` is usually followed by `in theorem ...` to limit the inclusion to the subsequent declaration.include 命令标记该变量。所有被标记的变量都会被无条件添加到所有定理中。 Lean.Parser.Command.omit : command`omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in which case all instance variables that unify with the given type are omitted. `omit` should usually only be used in conjunction with `in` in order to keep the section structure simple.omit 命令可用于去除变量的 include 标记；通常建议配合 Lean.Parser.Command.in : commandin 使用。

Included and Omitted Section Variables

本区段的变量包含了一个谓词以及用于证明其适用于所有自然数的条件，还加了一个多余的假设。

section
variable {p : Nat → Prop}
variable (pZero : p 0) (pStep : ∀ n, p n → p (n + 1))
variable (pFifteen : p 15)

但下例定理默认只加了 p 这个变量，导致无法证明：

theorem p_all : ∀ n, p n := unsolved goals
case zero
p : Nat → Prop
⊢ p 0

case succ
p : Nat → Prop
n✝ : Nat
a✝ : p n✝
⊢ p (n✝ + 1)byp:Nat → Prop⊢ ∀ (n : Nat), p n
  intro np:Nat → Propn:Nat⊢ p n
  induction nzerop:Nat → Prop⊢ p 0succp:Nat → Propn✝:Nata✝:p n✝⊢ p (n✝ + 1)

Lean.Parser.Command.include : command`include eeny meeny` instructs Lean to include the section `variable`s `eeny` and `meeny` in all theorems in the remainder of the current section, differing from the default behavior of conditionally including variables based on use in the theorem header. Other commands are not affected. `include` is usually followed by `in theorem ...` to limit the inclusion to the subsequent declaration.include 命令会无条件插入额外假设：

include pZero pStep pFifteen

automatically included section variable(s) unused in theorem 'p_all':
  pFifteen
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit pFifteen in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`theorem p_all : ∀ n, p n := byp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ ∀ (n : Nat), p n
  intro np✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n:Nat⊢ p n
  induction nzerop✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) <;>zerop✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp✝:Nat → ProppFifteen:p✝ 15p:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) simp [*]All goals completed! 🐙

由于插入了无意义的 pFifteen，Lean 会发出警告：

automatically included section variable(s) unused in theorem 'p_all':
  pFifteen
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit pFifteen in theorem ...
note: this linter can be disabled with `set_option linter.unusedSectionVars false`

为避免这个问题，可用 Lean.Parser.Command.omit : command`omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in which case all instance variables that unify with the given type are omitted. `omit` should usually only be used in conjunction with `in` in order to keep the section structure simple.omit 去掉 pFifteen 的 include 标记：

include pZero pStep pFifteen

omit pFifteen in
theorem p_all : ∀ n, p n := byp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ ∀ (n : Nat), p n
  intro np:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n:Nat⊢ p n
  induction nzerop:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) <;>zerop:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)⊢ p 0succp:Nat → ProppZero:p 0pStep:∀ (n : Nat), p n → p (n + 1)n✝:Nata✝:p n✝⊢ p (n✝ + 1) simp [*]All goals completed! 🐙

end